﻿Теоремы-следствия аксиом
admin|2009/01/18 18:03:57
##PAGE##
 Теоремы-следствия аксиом являются утверждениями которые доказываются на основе одного или нескольких алгебраических
законов. По сути, доказанную выше теорем у об эквивалентности
программ тоже можно отнести к этому классу законов. В качестве
примера данном разделе мы докажем полезную теорему о программах,
использующих хвостовую рекурсию. В заключительном разделе этой главы
теорема используется в рамках большого примера.

===Теорема о хвостовой рекурсии===
'''Теорема'''
 Для всех <math>n\geq1</math> и всех FP-программ
''f'',''a'', ''b'' и ''c'' верно равенство

<math>
[f,a\circ2]^n\circ[b,c]=[\backslash f\circ[b,c,a \circ
c,\ldots,a^{n-1}\circ c],a^n \circ c]
</math>

'''Доказательство.'''

 Индукцией по n.

''Базис индукции''
<math>f,a\circ 2]\circ[b,c]&=[f\circ[b,c],a\circ 2\circ[b,c]] </math> по [Axioms#IBB_10|I.11]

                       <math>=[f\circ[b,c],a\circ c] </math> по [I.5] если b определено
                                        и по <math> \bar{\bot}=\bar{\bot}</math>в противном случае

                       <math>=[f\circ[\backslash f\circ[b],c],a\circ c]</math> по [Axioms#IBA_10|I.11] для левой свертки

                       <math>=[\backslash f\circ[b,c],a\circ c]</math> по [Axioms#IBA_10|I.11] для левой свертки


''Шаг индукции''
 Для удобства и краткости записи определим выражение ''E'' как

<math>E = [\backslash f\circ[b,c,a\circ c,\ldots,a^{n-1}\circ c],a^n\circ c]</math>

 Получаем:
<math>[f,a\circ &2]^{n+1}\circ[b,c]</math>

           <math>=[f,a\circ2]\circ[f,a\circ2]^n\circ[b,c]</math> по определению <math>f^n</math>

           <math>=[f,a\circ2]\circ E</math>  по индукции

           <math>=[f\circ E,a\circ2\circ E]</math> по [I.1]

           <math>=[f\circ E,a\circ a^n\circ c]</math>по [I.5] если ''E'' определено''

                                          и по <math>\bar{\bot}=\bar{\bot}</math> в противном случае

           <math>=[f\circ E,a^{n+1}\circ c]</math> по определению <math>f^n</math>

           <math>=[\backslash f \circ[b,c,a\circ c,\ldots,a^n\circ c],a^{n+1}\circ c]</math> по [Axioms#IBB_10|I.11] для левой свертки
</math>
Теорема доказана.

 Еще раз подчеркнем, что теорема следует напрямую из свойств комбинирующих форм композиции, конструкции и свертки
и является общей для всех FP-программ ''f'', ''a'', ''b''
и ''c''.
